『Intuitionistic Type Theory (Stanford Encyclopedia of Philosophy)』
table:訳
英語 訳
constructive mathmatics 構成的数学 Zermelo-Fraenkel Set Theory ツェルメロ=フランケル集合理論(ZFC公理系) Brouwer-Heyting-Kolmogorov interpretation ブラウラー-ハイティング-コルゴロフ解釈(BHK解釈) table:目次
1. Overview 1. 概要
2. Propositions as Types 2. 型としての命題
2.1 Intuitionistic Type Theory: a New Way of Looking at Logic? 2.1 直観主義的型理論：論理学の新しい見方？ 2.2 The Curry-Howard Correspondence 2.2 カリー＝ハワード対応 2.3 Sets of Proof-Objects 2.3 証明対象の集合
2.4 Dependent Types 2.4 依存型 2.5 Propositions as Types in Intuitionistic Type Theory 2.5 直観主義型理論における型としての命題
3. Basic Intuitionistic Type Theory 3. 基本的な直観主義型理論
3.2 Judgment Forms 3.2 判断形式
3.3 Inference Rules 3.3 推論ルール
3.4 Intuitionistic Predicate Logic 3.4 直観主義述語論理 3.5 Natural Numbers 3.5 自然数
3.6 The Universe of Small Types 3.6 小さい型の宇宙
3.7 Propositional Identity 3.7 命題の同一性
3.8 The Axiom of Choice is a Theorem 3.8 選択の公理は定理である
4. Extensions 4. 拡張
4.1 The Logical Framework 4.1 論理的枠組み
4.2 A General Identity Type Former 4.2 一般的な同一型元(???)
4.3 Well-Founded Trees 4.3 根拠のある木(???)
4.4 Iterative Sets and CZF 4.4 反復集合とCZF
4.5 Inductive Definitions 4.5 帰納的定義
4.6 Inductive-Recursive Definitions 4.6 帰納的-再帰的定義
5. Meaning Explanations 5. 意味の説明
5.1 Computation to Canonical Form 5.1 正準形式への計算
5.2 The Meaning of Categorical Judgments 5.2 カテゴリー判断の意味
5.3 The Meaning of Hypothetical Judgments 5.3 仮説的判断の意味
6. Mathematical Models 6. 数学的モデル
6.1 Categorical Models 6.1 カテゴリー・モデル
6.2 Set-Theoretic Model 6.2 集合論的モデル
6.3 Realizability Models 6.3 実現可能性モデル
6.4 Model of Normal Forms and Type-Checking 6.4 正規形と型検査のモデル
7. Variants of the Theory 7. 理論の変形
7.1 Extensional Type Theory 7.1 拡張型理論
7.3 Partial and Non-Standard Type Theory 7.3 部分型と非標準型理論
7.4 Impredicative Type Theory 7.4 非正規型理論
7.5 Proof Assistants 7.5 証明支援
Bibliography 参考文献
Academic Tools 学術ツール
Other Internet Resources その他のインターネットリソース
Related Entries 関連項目